Definitions | event_system{i:l}, t T, x:A. B(x), es-E(es), es-locl(es; e; e'), prop{i:l}, P Q, l_before(x; y; l; T), before(e), P  Q, P  Q, P   Q,  b, , False, Unit, guard(T),  x. t(x), wellfounded{i:l}(A; x,y.R(x;y)), es-first(es; e), b, A, (x l), P Q, es-pred(es; e) |